ds, ds':ltg:Id fp Type. ds  ds'  State(ds')  State(ds) 

latex

Definitions	x:A. B(x), P  Q, S  T, t  T, x. t(x), x(s),
Lemmas	ma-state-subtype, ma-state wf, fpf-sub wf, Id wf, id-deq wf, fpf wf